However, to deal with ambiguity and partial information, new approache s have emerged - examples of which are fuzzy logic, probabilistic modal logic, Bayesian networks and belief-based systems. Even though progress has been made, these approaches genera lly have a limitation: the probability or degree of belief, in general, being kept out of the l ogical semantics, remaining at another level of interpretation on a deterministic model. In other w ords, maintaining the binary characteristic of truth - true or false, with uncertainty being treate d as associated with models, rather than a property of logical language in itself. The proposed logic will be used to solve the problem of tackling certain types of uncertainty and imprecision with Bayesian Networks. The aim is to take advantage of the conceptual and practical benefits of this sy stem in practical situations that have not yet been adequately explored.

This paper seeks to apply categorical logic to the design of artificial intelligent agents that reason symbolically about objects more richly structured than sets. Using Johnstone's sequent calculus of terms- and formulae-in-context, we develop forward chaining and normal form algorithms for reasoning about objects in cartesian categories with the rules for Horn logic. We also adapt first-order unification to support multi-sorted theories, contexts, and fragments of first-order logic. The significance of these reformulations rests in the fact that they can be applied to reasoning about objects in semantic categories that do not support classical logic or even all its connectives.

The ideas that he raised in his study of logical reasoning carried the development of science over the centuries. Any scientific theory's mathematical formalization is one that falls under his idea of Demonstrative Science. T oday, in the era of AI, this title of the fatherhood of logic has a renewed significance . Behind it li es his original idea that human reasoning c ould be studied as a process and that perhaps there exist universal systems of reasoning that underly all human reasoning irrespective of the content of what we are reasoning about . This is a daring idea as it ess entially says that the human mind can study itself and indeed that it has the capacity to unravel its own self. Irrespective of whether this is possible or not, it is a thought that is a prerequisite for the existence and development of Artificial Intellig ence. In this article, we look into Aristotle's work on human thought, his work on reasoning itself but also on how it relates to science and human endeavour more generally, from a modern perspective of Artificial Intelligence and ask if this can help enli ghten our understanding of AI and S cience more generally.

With the increase in industrial applications using Answer Set Programming, the need for formal verification tools, particularly for critical applications, has also increased. During the program optimisation process, it would be desirable to have a tool which can automatically verify whether an optimised subprogram can replace the original subprogram. Formally this corresponds to the problem of verifying the strong equivalence of two programs. In order to do so, the translation tool anthem was developed. It can be used in conjunction with an automated theorem prover for classical logic to verify that two programs are strongly equivalent. With the current version of anthem, only the strong equivalence of positive programs with a restricted input language can be verified. This is a result of the translation $\tau^*$ implemented in anthem that produces formulas in the logic of here-and-there, which coincides with classical logic only for positive programs. This thesis extends anthem in order to overcome these limitations. First, the transformation $\sigma^*$ is presented, which transforms formulas from the logic of here-and-there to classical logic. A theorem formalises how $\sigma^*$ can be used to express equivalence in the logic of here-and-there in classical logic. Second, the translation $\tau^*$ is extended to programs containing pools. Another theorem shows how $\sigma^*$ can be combined with $\tau^*$ to express the strong equivalence of two programs in classical logic. With $\sigma^*$ and the extended $\tau^*$, it is possible to express the strong equivalence of logic programs containing negation, simple choices, and pools. Both the extended $\tau^*$ and $\sigma^*$ are implemented in a new version of anthem. Several examples of logic programs containing pools, negation, and simple choice rules, which the new version of anthem can translate to classical logic, are presented. Some a...

In classical logic, "P implies Q" is equivalent to "not-P or Q". It is well known that the equivalence is problematic. Actually, from "P implies Q", "not-P or Q" can be inferred ("Implication-to-disjunction" is valid), while from "not-P or Q", "P implies Q" cannot be inferred in general ("Disjunction-to-implication" is not generally valid), so the equivalence between them is invalid in general. This work aims to remove exactly the incorrect Disjunction-to-implication from classical logic (CL). The paper proposes a logical system (IRL) with the expected properties: (1) CL is simply obtained by adding Disjunction-to-implication to IRL, and (2) Disjunction-to-implication is independent of IRL (either Disjunction-to-implication or its negation cannot be derived in IRL) in the general case. In other words, IRL is just the system obtained by exactly removing Disjunction-to-implication from CL.

The Weak Completion Semantics (WCS) is a computational cognitive theory that has shown to be successful in modeling episodes of human reasoning. As the WCS is a recently developed logic programming approach, this paper investigates the correspondence of the WCS with respect to the well-established Answer Set Semantics (ASP). The underlying three-valued logic of both semantics is different and their models are evaluated with respect to different program transformations. We first illustrate these differences by the formal representation of some examples of a well-known psychological experiment, the suppression task. After that, we will provide a translation from logic programs understood under the WCS into logic programs understood under the ASP. In particular, we will show that logic programs under the WCS can be represented as logic programs under the ASP by means of a definition completion, where all defined atoms in a program must be false when their definitions are false.

LPMLN is a probabilistic extension of answer set programs with the weight scheme adapted from Markov Logic. We study the concept of strong equivalence in LPMLN, which is a useful mathematical tool for simplifying a part of an LPMLN program without looking at the rest of it. We show that the verification of strong equivalence in LPMLN can be reduced to equivalence checking in classical logic via a reduct and choice rules as well as to equivalence checking under the "soft" logic of here-and-there. The result allows us to leverage an answer set solver for LPMLN strong equivalence checking. The study also suggests us a few reformulations of the LPMLN semantics using choice rules, the logic of here-and-there, and classical logic.

Argumentation is a non-monotonic process. This reflects the fact that argumentation involves uncertain information, and so new information can cause a change in the conclusions drawn. However, the base logic does not need to be non-monotonic. Indeed, most proposals for structured argumentation use a monotonic base logic (e.g. some form of modus ponens with a rule-based language, or classical logic). Nonetheless, there are issues in capturing defeasible reasoning in argumentation including choice of base logic and modelling of defeasible knowledge. And there are insights and tools to be harnessed for research in non-monontonic logics. We consider some of these issues in this paper.

One purpose of CASC is to provide a public evaluation of the relative capabilities of ATP systems. The TPTP version used for CASC is released beyond the ATP community. Fulfillment of these after the competition, so that new problems have not objectives provides insight and stimulus for the been seen by the entrants. In some divisions the systems development of more powerful ATP systems, leading are ranked according to the number of problems to increased and more effective use. The most recent CASC, accompanied by a proof or model (thus giving only held at CADE-25 in Berlin, Germany, in 2015, was an assurance of the existence of a proof/model).

We consider knowledge representation (KR) formalisms as collections of finite knowledge bases with a model-theoretic semantics. In this setting, we show that for every KR formalism there is a formalism that characterizes strong equivalence in the original formalism, that is unique up to isomorphism and that has a model theory similar to classical logic.